Comments on:

	  Voevodsky
	  C-system of a module over a Jf-relative monad
	  2016_01_31_Csystemfromamonad.pdf

The introduction is much improved since the previous version, and the editor
may wish to read it.

The current paper has 32 pages, and is part of a longer sequence of papers
designed to prove the soundness of univalent type theory in the presence of the
univalence axiom, the law of the excluded middle, and the axiom of choice.
Part of the proof concerns the realization of the univalence axiom as a
property about simplicial sets, and part of the proof relates the formal
language of univalent type theory to a mathematical structure of its syntax,
which can them be modeled in topology to prove soundness.  This paper covers
some of the latter part.

The long study of the mathematics of computer language syntax has resulted in 5
equivalent notions, all of which are treated in detail or mentioned in this
paper:

  - l-bijective C-systems
  - Lawvere theories
  - Jf-relative monads
  - abstract clones
  - substitution systems (or substitution algebras?)

Type theoretically they all correspond to type theories where there is just one
type, which might be taken to be the type of raw terms underlying the (more
interesting) type theory to be studied.  One expects the formalism of the raw
syntax of terms to be elementary, so the proliferation of these concepts is
unexpected and confusing.

The isomorphism between the category of l-bijective C-systems and the category
of Lawvere theories is described in Voevodsky's 15 page preprint [17].  The
equivalence between the category of Lawvere theories and the category of
Jf-relative monads is established in Voevodsky's 21 page preprint [21].  The
current paper uses both of those to perform some computations.

The mathematics in the current paper is straightforward, the proofs are easy,
and the concepts are concrete, yet bulky and unfamiliar to mathematicians,
since they are oriented toward dealing with the syntax of formal languages in a
mathematical way.  Thus the typical mathematician will find the paper rough
going, since it is long, and the main reward from reading it is to come far in
the future, after the "initiality conjecture" is proved, thereby establishing
the soundness of univalent type theory.

Theorems 5.12 and 6.10 are the only theorems of the paper, and each one is
simply a long list of formulas.  I didn't read them carefully or check them --
the proofs are presented in detail.  We take on faith that the formulas will be
useful later, and are offered this reassurance in the introduction: "In the
next paper we will connect these computations to the conditions that the valid
judgements of a type theory must satisfy in order for the term C-system of this
type theory to be defined".  I ask for more details in my remarks below.

I expect the initiality conjecture will be proved eventually, and when that
happens, this paper will be an important part of the proof of the soundness of
univalent type theory, which will be an essential and important foundational
result in the field.

The main question in my mind, as referee, is whether the preprints (there are
nine at this point), including this one, should instead be combined into a
large future monograph that would contain the crowning theorem.  I've mulled
this over for some minutes and decided "no" -- the individual preprints, while
not offering much reward for reading them now, offer accessible segments of the
whole, each with a certain unity to them.  There are also some advantages to
having the work reach the devoted followers early, as its pieces are
accomplished.  Think of them as chapters in a serial novel.

I recommend publication in JPAA.

-----------------------------------------------------------------------------

MATHEMATICAL REMARKS:

Theorems 5.12 and 6.10 are the only theorems of the paper, and each one is
simply a long list of formulas.  We take on faith that the formulas will be
useful later, and are offered this reassurance in the introduction: "In the
next paper we will connect these computations to the conditions that the valid
judgements of a type theory must satisfy in order for the term C-system of this
type theory to be defined".  Could something more be said here to give the
reader an inkling of why such formulas might be useful?  For example, is the
form of the formulas somehow closer to the way inference rules for a type
theory are traditionally formulated?

What is the type-theoretic motivation for the construction CC[F], introduced on
page 7?  Oh, the answer comes much later, on page 25: "The role of these
C-systems in the theory of type theories is that the term C-systems of the raw
syntax of dependent type theories are of this form and therefore the term
C-systems of dependent type theories are regular sub-quotients of such
C-systems and can be studied using the description of the regular sub-quotients
given in [20]."  It would be good for the reader to have an indication of that
earlier, perhaps all of it, or perhaps something along the lines of "CC will
capture the raw syntax of terms of a type theory, F will capture the raw syntax
of types, and CC[F] will encode them together", if I have that right.

Jf is well behaved in the sense of [2, section 4], so any relative monad for it
extends to a monad on the category of sets, as is proved there.  This seems to
answer the question in remark 4.6, which is reserved for a future paper, unless
the proof there implicitly uses LEM.

Near "Example 6.2 An important example of LM is given by ..." it might be good
to say why it's important, from the point of view of type theory.  Does it have
to do with the possibility of not distinguishing initially between terms for
elements and terms for types, throwing them all into CC, and then using the
construction CC[LM] to create the C-system for the raw syntax of contexts?

-----------------------------------------------------------------------------

MINOR STYLISTIC REMARKS:

the o in Martin-Lof in the bibliography is typeset incorrectly

in "For the two of the several main groups of inference rules" omit the first
"the"

Change "This allows to avoid the use of natural numbers in some of the
arguments that significantly simplifies the proofs" to "This allows us to avoid
the use of natural numbers in some of the arguments, thereby significantly
simplifying the proofs."

Change "The C-systems of this form remind in some way the affine spaces over
schemes in algebraic geometry" to "The C-systems of this form remind us in some
way of affine spaces over schemes in algebraic geometry."

remove hyphens from "sub-space" and "sub-quotient"

remove "very" from "not very interesting"

add the indicated comma in "While the geometry of affine spaces in itself is
not very interesting, their sub-spaces encompass all affine algebraic varieties
of finite type."

remove spaces before periods at ends of sentences: "... finite type ."

change "look to be" to "seem to be"

change "not very different from CC" to "similar to CC".  The reason is that
"not very different" is ambiguous: it could be the negation of "very
different", or it could mean "only slightly different".  Also, "very" is an
overused qualifier in English prose, often used with no clear intent.

I find "Regular sub-quotients of any C-system CC are classified by ... " abrupt
because "regular subquotients" are not mentioned in [20].  Of course, one can
guess what it is, but why make the reader guess?  At this point, it is probably
useful to remind the reader that the result stated is covered in [20], if it
is, and to provide a citation.  If it's not in [20], then why is it true?

change "we first remind the notion of a relative monad on" to "we first recall
the notion of a relative monad on".  Every use of "remind" without mentioned
the persons being reminded should be replaced by "recall", or the persons
should be mentioned: "We recall the notion X"; "We remind the reader of the
notion X".

add the indicated commas: "Since this paper, as well as other papers in the
series on C-systems, is expected to play a role in the mathematically rigorous
construction of the simplicial univalent representation of the UniMath language
and the Calculus of Inductive Constructions, and since such a construction
itself can not rely on the univalent foundations, the paper is written from the
perspective of the Zermelo-Fraenkel formalism."

in "The paper is written in the formalization-ready style" the second "the" is
inappropriate, because there can be multiple styles ready for formalization.
Avoid hyphens.  How about this?: "The paper is written in a style that should
lend itself to straightforward formalization."

The sentence "In all that follows we write Sets instead of Sets(U)" would be
clearer if one didn't have to guess the meaning of "Sets(U)", and if "Sets"
hadn't already been written previously.  Just say that "We let Sets denote the
category of sets in U", or give a forward reference to the definition of
Sets(U) in the body of the paper.

change "Recall that for a C-system CC, and object Γ of CC such that l(Γ) ≥ i we
..." by inserting "an", inserting a comma, and removing a comma, to get "Recall
that for a C-system CC and an object Γ of CC such that l(Γ) ≥ i, we ...".  The
reason for removing the first comma is that the "and" is separate two noun
phrases, not clauses.  The second comma helps the tired reader.

change "... define a pair of an object and a morphism defined inductively as
..." to "... denote the object and the morphism defined inductively by ...".
The point is that a definition associates notation to a mathematical object,
after which the notation denotes the object.  Moreover, neither notation refers
to a pair, we have just two notations for two objects.

In "If Γ′ is over Γ" it seems that "is over" is being used instead of " > " or
" \ge ", but the reader must guess it, as it is nonstandard, so define it.
Better than "over" would be "above", because "over" already has a meaning in
any category, e.g., a scheme X over S.

In the statement of lemma 2.2, the reader can deduce that Gamma' and Gamma''
are over Gamma''', because "a" is, but why make the reader do that?  Better
would be to start with a over Gamma''' and Gamma''' over Delta, and deduce that
a is also over Delta.

It seems odd that "Construction 3.2" is the construction corresponding to
"Problem 3.1".  Why not use the same number for both?  Then it would be clear
to the reader that they correspond.

change "where () is the unique element of the one point set that is the product
of the empty sequence" to "where () is the unique element of the one point set,
the empty sequence", because "product of the" is not applicable here.

before "which is well defined because" put a comma.

in remark 3.5 C[F] should be CC[F]

in remark 3.6 mathematicians will have to guess that "unit" refers to the one
element set

change "remind" to "recall" in "Let us remind it here."

This word order is clumsy: "The set of Jf-relative monads is in an easy to
construct bijection with the set of abstract clones as defined in [6, Section
3]."  I suggest "There is a bijection between the set of Jf-relative monads and
the set of abstract clones as defined in [6, Section 3]."  Avoid saying "easy"
or "straightforward" whenever possible, since readers differ in ability.

It might be good to say that Construction 4.3 occurs in [2].

In problem 4.4 a reference is given to p.133 of [10].  The reader must guess
that the reference is given as a source for the definition of "monad", and will
be misled by the use of "cf." when there is nothing in the text to compare with
what's in the reference.  See "https://en.wikipedia.org/wiki/Cf.".  Perhaps
simply precede the problem with a sentence saying that the definition of monad
can be found in [10, p. 133].

The paragraph beginning "Recall that the category T has as ..." will seem
overly pedantic to a mathematician, who will be comfortable with the looser
phrasing "we identify ((m,n),f) with f when it will cause no confusion", and
will take it to imply the needed coercions.

In "The proof of the composition and the identity axioms of a functor are easy"
we have the subject "proof", which is singular, and the verb "are", which is
plural.  Avoid saying "easy" or "straightforward" whenever possible, since
readers differ in ability.  Say just that the proof is omitted or that it is
left to the reader.

change "We will only consider the case when U is a universe" to "We will
consider only the case when U is a universe."

Remark 4.8 can be safely eliminated.

Change "the opposite category to T" to "the opposite category of T".

Insert the indicated comma: "previous section, the most important of which ..."

This sentence is impossible to understand: "In the final Section 6 we apply the
construction of Section 3 to C(RR) taking into account that the functors LM :
C(RR)op → Sets are the same as the functors K(RR) → Sets that are the same as
the relative (left) modules over Jf."

Clearer than
"In (25) and Construction 6.8 we compute the B-sets B(C(RR,LM)) and B
(C(RR,LM)) and in Theorem 6.10 the action of the B-system operations on these
sets."
would be
"In (25) and Construction 6.8 we compute the B-sets B(C(RR,LM)) and B
(C(RR,LM)), and in Theorem 6.10 we compute the action of the B-system operations on these
sets."

The sentence "Combining this conjecture with Theorem 5.12 we conclude ..."
sounds strange, because conjectures don't allow you to conclude anything.
Maybe say something like "The assumption that the conjecture is true, along
with Theorem 5.12, would allow us to conclude ..."

The author writes "the category of abstract clones is equivalent to the
category of substitution systems of [6, Definition 3.1]."  But the cited
definition defines "substitution algebras", not "substitution systems".

Remove "the" from "left modules over ... are the presheaves on C(RR)"
and from "i.e., the contravariant functors ... ", or insert it before "left
modules".

Remove "the" from "can be thought of as the substitution."

Near "Modules (actually left modules) over relative monads were introduced in
[1, Definition 9]" it might be good to attribute the notion of left modules
over monads to the appropriate paper of Hirschowitz and Maggesi, as was done in
the first version of the paper.

The sentence "One can verify that for any Jf-relative monad RR, ψ = σ where σ
is the permutation of 0 and 1 in stn(2)" doesn't quite make sense, because ψ :
RR(2) -> RR(2), whereas σ : stn(2) -> stn(2).  One could say instead that "One
can verify that for any Jf-relative monad RR, ψ is induced by the transposition
of 0 and 1 in stn(2)."

In "we have for each m,n ∈ N a function R(n,m) → ..."  replace "R(n,m)" by
"RR(n,m)".

In the remark "we can define a left l-module lLM over RR as a quadruple ..." I
wonder what "l" refers to.  I realize that there is also something called "l"
in the following definition, but that can't be the same "l", or else it would
been introduced earlier.  I'm also confused because one would expect terms such
as "left module over RR" and "left RR-module" to be used instead, and to be
equivalent.

We also see "These l-versions of the relative monads and their modules ... "
and are in the dark about what an "l-version" of something is.

That remark continues: "we can define a left l-module lLM over RR as a
quadruple ... where operations l, ∂ and θLM satisfy some conditions.  Once
these conditions are properly established ... ".  The conditions are never
listed.  It is important to warn the reader at an earlier stage by saying
something like this instead: "we would like to be able to define a left
l-module lLM over RR as a quadruple ..."

change "for a particular class of the inference rules" to "for a particular
class of inference rules"

This sentence tantalizes: "The term models for a class of type theories can be
obtained by considering slices of the term model of the type theory called
Logical Framework (LF), but unfortunately it is unclear how to extend this
approach to type theories that have more substitutional (definitional)
equalities than LF itself."  Is the work published?  If so, where?  Who did the
work?

in "obtained by considering slices of the term model of the type theory called
Logical Framework" is the word "slices" being used in a technical sense?  If
not, it's confusing.  If so, a footnote giving a reference to the definition
would be appropriate, or one could rephrase the sentence to make it
self-evident how to read it.

Change "At the time when that paper was written" to "At the time that paper was
written" or to "When that paper was written", to eliminate redundancy.

insert the indicated comma: " body of work on type theory, which is reflected "

in "(cf. also [9, Example 1.2.3] that claims as ... " I suspect "cf." is being
used to mean "see".  If so, change it to "see", because "cf." means "compare".
Then put a comma before "that" and change "that" to "which".

I see both "relative monad *on* a functor" and "relative monad *over* the
functor".  It would be good to pick "on" or "over" and to use it uniformly.

In "In the next paper we will connect these computations to the conditions that
the valid judgements of a type theory must satisfy in order for the term
C-system of this type theory to be defined" change "this" to "the", or better,
rephrase as "In the next paper we will connect these computations to the
conditions that the valid judgements of a type theory must satisfy in order for
its term C-system to be defined."